$\forall$$i$:Id, $X$, $T$:Type, $x_{0}$:$X$, $P$:($X$$\rightarrow$$T$$\rightarrow$Prop).
\\[0ex]Normal($T$)
\\[0ex]$\Rightarrow$ Normal($X$)
\\[0ex]$\Rightarrow$ ($\forall$$x$:$X$. Dec($\exists$$v$:$T$. $P$($x$,$v$)))
\\[0ex]$\Rightarrow$ preinit1R\{x:ut2, a:ut2\}($i$; $X$; $T$; $x_{0}$; $P$) $\in$ Realizer